$\forall$$T$:Type, $P$:(($T$ List)$\rightarrow$Prop), $L$:$T$ List, $x$:$T$.
\\[0ex]($\exists$$L_{1}$:$T$ List. $L_{1}$ $\leq$ $L$ @ [$x$] \& $P$($L_{1}$)) \& $\neg$($\exists$$L_{1}$:$T$ List. $L_{1}$ $\leq$ $L$ \& $P$($L_{1}$))
\\[0ex]$\Leftrightarrow$
\\[0ex]$P$($L$ @ [$x$]) \& $\neg$($\exists$$L_{1}$:$T$ List. $L_{1}$ $\leq$ $L$ \& $P$($L_{1}$))